Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

a(a(x1)) → a(b(b(b(x1))))
b(a(x1)) → b(b(c(x1)))
a(b(b(c(x1)))) → a(a(a(b(x1))))

Q is empty.


↳ QTRS
  ↳ RFCMatchBoundsTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

a(a(x1)) → a(b(b(b(x1))))
b(a(x1)) → b(b(c(x1)))
a(b(b(c(x1)))) → a(a(a(b(x1))))

Q is empty.

Termination of the TRS R could be shown with a Match Bound [6,7] of 4. This implies Q-termination of R.
The following rules were used to construct the certificate:

a(a(x1)) → a(b(b(b(x1))))
b(a(x1)) → b(b(c(x1)))
a(b(b(c(x1)))) → a(a(a(b(x1))))

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

1, 2, 4, 3, 7, 6, 5, 10, 9, 8, 12, 11, 15, 14, 13, 18, 17, 16, 21, 20, 19, 23, 22, 25, 24, 28, 27, 26, 31, 30, 29, 33, 32, 35, 34, 38, 37, 36, 41, 40, 39, 44, 43, 42, 46, 45, 48, 47, 50, 49, 59, 58, 57, 61, 60, 63, 62

Node 1 is start node and node 2 is final node.

Those nodes are connect through the following edges: